﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\OnlineAlgo\NFMs\L_Plus_M.cs
 * Description  :     Implementation of Observation Pack Algorithm 
 *                    (based on Finally.M.Hoar work [PhD thesis title: Active learning of interface programs])
 * Change log   :     -8 May 2013: Some preliminary implementation
 * To Do        :     -Not implemented completely YET!
 ************************************************************************/

using System;
using System.Collections.Generic;

using AIDE.Utils;
using SMLib.Automata.Base;
using SMLib.Automata.MM;
using AIDE.Oracles.NFMs;


namespace AIDE.OnlineAlgo.NFMs
{
    /// <summary>
    /// Observation Pack Algorithm 
    /// [based on Finally.M.Hoar work, PhD thesis title: "Active learning of interface programs" (2012)]
    /// </summary>
    public class Observation_Pack: INFM_Learner
    {
        IOracle_MAT_MM myOracle;
        List<Component> components;

        /// <summary>
        /// Constructor
        /// </summary>
        /// <param name="oracle">the MAT oracle</param>
        public Observation_Pack(IOracle_MAT_MM oracle)
        {
            this.myOracle = oracle;
            policy = CounterexampleHandlingPolicy.allGlobally;
        }



        #region Discrimination Tree
        /// <summary>
        /// [P.12 of thesis]
        /// </summary>
        class Component
        {
            public Component()
            {
                Table = new List<row>();
                suffixes = new List<Word>();
            }
            public bool ContainsPrefix(Word pref)
            {
                foreach (row r in this.Table)
                {
                    if (r.prefix.Equals(pref))
                        return true;
                }
                return false;
            }
            /// <summary>
            /// One row of observation table in the component
            /// </summary>
            public class row
            {
                public row(Word prefix = null)
                {
                    if (prefix != null)
                        this.prefix = prefix;
                    else
                        this.prefix = new Word();
                    rowValues = new List<ISymbol>();
                }

                public Word prefix;
                public List<ISymbol> rowValues;
            }

            public List<Word> suffixes;
            public List<row> Table;
            public Tree<Word, ISymbol>.TreeNode correspondingNode;


            /// <summary>
            /// Check whether the component is closed or not.
            /// </summary>
            /// <returns></returns>
            public int isClosed(out int notClosedRow, out int notClosedCol)
            {
                notClosedRow = notClosedCol = -1;
                if (Table.Count == 0)
                    return -1;
                for (int i = 1; i < Table.Count; i++)
                {
                    for (int j = 0; j < suffixes.Count; j++)
                    {
                        if (!Table[i].rowValues[j].Equals(Table[0].rowValues[j]))
                        {
                            notClosedRow = i;
                            notClosedCol = j;
                            return i;
                        }
                    }
                }
                return -1;
            }

            /// <summary>
            /// (unique) Access sequence
            /// </summary>
            public Word U0
            {
                get
                {
                    return Table[0].prefix;
                }
            }
        }


        Tree<Word, ISymbol> discrTree;
        #endregion

        /// <summary>
        /// Get component corresponding to a leaf
        /// </summary>
        /// <param name="u">access string of the component</param>
        /// <returns>the corresponding component</returns>
        Component Lambda(Word u)
        {
            foreach (Component c in components)
            {
                if (c.U0.Equals(u))
                    return c;
            }
            return null;
        }

        void AddPrefixToComponent(Component c, Word prefix)
        {
            c.Table.Add(new Component.row(prefix));
            int index = c.Table.Count - 1;
            for (int i = 0; i < c.suffixes.Count; i++)
            {
                Word O = myOracle.OutputTrace(prefix, c.suffixes[i]);
                c.Table[index].rowValues.Add(O[O.Length - 1]);
            }
        }

        /// <summary>
        /// Sift a word in the tree [Based on Sift algorithm P.14 of the thesis]
        /// <remarks>A new word u is sifted into the observation pack, by sinking it into the
        /// discrimination tree. At each inner node on the path from the root a membership query is
        /// performed for the concatenation of u and the suffix v labeling the node. The outcome
        /// of the membership query determines which edge to follow. New words are added
        /// as prefixes to the component that corresponds to the leaf reached when sifting the word into
        /// the tree.</remarks>
        /// </summary>
        /// <param name="u">the new component (if it makes a new one) or null (if it was sifted in an existing component)</param>
        /// <returns></returns>
        Component Sift(Word u)
        {
            //* 1-star from root
            Tree<Word, ISymbol>.TreeNode currNode = discrTree.Root;
            Component selectedComp = null;

            bool found;
            List<Word> allSuffixes = new List<Word>();
            while (true)
            {
                //* Reaching to a leaf
                if (currNode.Childs.Count == 0)
                {
                    found = true;
                    selectedComp = Lambda(currNode.NodeObject);
                    //* 16-Add prefix to component
                    AddPrefixToComponent(selectedComp, u);
                    return null;
                }

                found = false;
                //* 3-Get suffix for node
                Word v = currNode.NodeObject;
                allSuffixes.Add(v);
                //* 4-Check suffix on prefix
                Word o = myOracle.OutputTrace(u, v);

                foreach (ISymbol e in currNode.Edges)
                {
                    if (e.Equals(o[o.Length - 1]))
                    {
                        currNode = currNode.ChildByEdge(e);
                        found = true;
                        break;
                    }
                }

                if (!found)
                {
                    //* 9-Update tree, Update labels
                    Tree<Word, ISymbol>.TreeNode node = currNode.AddChild(u, o[o.Length - 1]);


                    //* 10-create new component
                    selectedComp = new Component();
                    selectedComp.correspondingNode = node;

                    components.Add(selectedComp);
                    selectedComp.suffixes.AddRange(allSuffixes);

                    AddPrefixToComponent(selectedComp, u);

                    return selectedComp;
                }
            }
        }

        /// <summary>
        /// Check whether two rows are equivalent or not
        /// </summary>
        /// <param name="r1"></param>
        /// <param name="r2"></param>
        /// <returns></returns>
        int EqualRows(Component.row r1, Component.row r2)
        {
            if (r1.rowValues.Count != r2.rowValues.Count)
                throw new Exception("Two rows don't have the same number of columns!");
            for (int i = 0; i < r1.rowValues.Count; i++)
            {
                if (!r1.rowValues[i].Equals(r2.rowValues[i]))
                    return i;
            }
            return -1;
        }



        Component Split(Component c, int indexOfU, int indexOfV)
        {
            ISymbol labelOfC = c.Table[0].rowValues[indexOfV];
            ISymbol labelOfCu = c.Table[indexOfU].rowValues[indexOfV];
            Word u = c.Table[indexOfU].prefix;
            Word v = c.suffixes[indexOfV];

            Tree<Word, ISymbol>.TreeNode nodeOfC = c.correspondingNode;

            //* 1-Create component Cu = ⟨∅, u, V , ∅⟩ in C
            Component c_u = new Component();
            c_u.suffixes.AddRange(c.suffixes);
            //c_u.Table.Add(new Component.row(u));
            components.Add(c_u);

            int i = 1;
            //* 2-Transfer prefixes
            while (i < c.Table.Count)
            {
                if (EqualRows(c.Table[i], c.Table[0]) >= 0)
                {
                    c_u.Table.Add(c.Table[i]);
                    c.Table.RemoveAt(i);
                }
                else
                    i++;
            }

            /*n_u*/
            Tree<Word, ISymbol>.TreeNode N_U = nodeOfC.AddChild(nodeOfC.NodeObject, labelOfC);
            c.correspondingNode = N_U;

            /*n_v*/
            Tree<Word, ISymbol>.TreeNode N_V = nodeOfC.AddChild(u, labelOfCu);
            c_u.correspondingNode = N_V;

            //* 11-Add new suffix to labels
            nodeOfC.SetNodeObject(v);
            //* (12-19) is automatically updated
            return c_u;
        }

        /// <summary>
        /// 
        /// </summary>
        /// <param name="c"></param>
        /// <param name="u"></param>
        /// <param name="v"></param>
        /// <returns></returns>
        Component Split(Component c, Word u, Word v)
        {
            //* before changinge the tree
            int indexOfV = -1;
            //ISymbol l1
            for (int j = 0; j < c.suffixes.Count; j++)
            {
                if (c.suffixes[j].Equals(v))
                {
                    indexOfV = j;
                    break;
                }
            }

            int indexOfU = -1;
            for (int j = 1; j < c.Table.Count; j++)
            {
                if (c.Table[j].prefix.Equals(u))
                {
                    indexOfU = j;
                    break;
                }
            }

            return Split(c, indexOfU, indexOfV);
        }

        /// <summary>
        /// Construct the conjecture from the discremination tree
        /// </summary>
        /// <returns>the conjecture</returns>
        MealyMachine ConstructConjecture()
        {
            MealyMachine conj = new MealyMachine();
            conj.InputAlphabet = myOracle.InputAlphabet;

            for (int i = 0; i < components.Count; i++)
            {
                conj.AddState(new MealyMachine.Mealy_State(i.ToString()));
            }

            for (int i = 0; i < components.Count; i++)
            {
                for (int j = 0; j < myOracle.InputAlphabet.Size; j++)
                {
                    ISymbol inpu = myOracle.InputAlphabet.AllSymbols()[j];
                    ISymbol outp = components[i].Table[0].rowValues[j];

                    MealyMachine.Mealy_State dest = null;
                    for (int k = 0; k < components.Count; k++)
                    {
                        Word w = components[i].U0.Clone();
                        w.AddSymbol(inpu);
                        if (components[k].ContainsPrefix(w))
                        {
                            dest = (MealyMachine.Mealy_State)conj[k];
                            break;
                        }
                    }
                    if (dest == null)
                    {
                        throw new Exception("Oops!");
                    }
                    ((MealyMachine.Mealy_State)conj[i]).AddTransition(dest, inpu, outp);
                }
            }
            return conj;
        }

        /// <summary>
        /// [P.16]
        /// </summary>
        /// <returns>Hypothesis</returns>
        MealyMachine ClosePack()
        {
            //* 1-Init. list of new (not-processed) components
            List<Component> W = new List<Component>();
            //* only in first iteration: W := {Cε}
            if (components.Count == 1)
            {
                W.Add(components[0]);
            }

            //* 2-Loop until stable
            while (true)
            {
                Component notClosedComponent = null;
                int unClosedRowIndex = -1, unClosedColIndex = -1;
                for (int i = 0; i < components.Count; i++)
                {
                    if (components[i].isClosed(out unClosedRowIndex, out unClosedColIndex) >= 0)
                    {
                        notClosedComponent = components[i];
                        break;
                    }
                }

                if (W.Count == 0 && notClosedComponent == null)
                {
                    return ConstructConjecture();
                }
                if (notClosedComponent != null)
                {
                    //* 5-Split componen
                    Component nC =
                        Split(notClosedComponent, notClosedComponent.Table[unClosedRowIndex].prefix,
                        notClosedComponent.suffixes[unClosedColIndex]);

                    //* 6-Add new component to W
                    W.Add(nC);
                }

                while (W.Count != 0)
                {
                    //* 8-Remove new component from W
                    Component c_u = W[0];
                    W.RemoveAt(0);
                    //* 9-
                    foreach (ISymbol a in myOracle.InputAlphabet.AllSymbols())
                    {
                        //* 10-Sift new prefixes to components
                        Word U = c_u.U0.Clone();
                        U.AddSymbol(a);
                        Component NC = Sift(U);
                        //* 11-Sifted to new component?
                        if (NC != null)
                        {
                            //* 12-Then: add new component to W
                            W.Add(notClosedComponent);
                        }
                    }
                }
            }
        }


        #region Handling counterexample

        CounterexampleHandlingPolicy policy;

        public enum CounterexampleHandlingPolicy
        {
            allGlobally,
            oneGlobally,
            oneLocally
        }

        public void SetPolicy(CounterexampleHandlingPolicy policy)
        {
            this.policy = policy;
        }



        void AddSuffixToComponent(Component c, Word suff)
        {
            c.suffixes.Add(suff);
            foreach (Component.row r in c.Table)
            {
                Word O = myOracle.OutputTrace(r.prefix, suff);
                r.rowValues.Add(O[O.Length - 1]);
            }
        }


        //Word Suffix4OneLocally(Word counterexample)
        //{
        //    int lowerBound = 0, higherBound = counterexample.Length, index;
        //    while (true)
        //    {
        //        index = (lowerBound + higherBound) / 2;
        //        Word myuff = counterexample.Suffix(counterexample.Length - index);
        //    }
        //}

        Word FindLongestSuffix(Word counterexample)
        {
            int maxL = 0;
            foreach (Component c in components)
            {
                for (int i = 0; i < c.Table.Count; i++)
                {
                    int l = c.Table[i].prefix.PrefixLength(counterexample);
                    if (l > maxL)
                        maxL = l;
                }
            }
            return counterexample.Suffix(counterexample.Length - maxL);
        }

        /// <summary>
        /// Handling counterexample [p.20]
        /// </summary>
        /// <param name="c">the counterexample</param>
        void HandleCounterexample(Word c)
        {
            switch (policy)
            {
                case CounterexampleHandlingPolicy.allGlobally:
                    Word suf = FindLongestSuffix(c);
                    //* 12-Add all suffixes of wc to V of all C ∈ C
                    foreach (Component comp in components)
                    {
                        for (int i = 2; i <= suf.Length; i++)
                        {
                            Word w = suf.Suffix(i);
                            if (comp.suffixes.Contains(w))
                                continue;
                            comp.suffixes.Add(w);
                            //* fill the table
                            foreach (Component.row r in comp.Table)
                            {
                                Word o = myOracle.OutputTrace(r.prefix, w);
                                r.rowValues.Add(o[o.Length - 1]);
                            }
                        }
                    }
                    break;
                case CounterexampleHandlingPolicy.oneGlobally:
                    //* 15-Add v to V of all C ∈ C
                    //Word V = null;
                    //foreach (Component comp in components)
                    //{
                    //    //* add the row
                    //    comp.suffixes.Add(V);
                    //    //* fill the table
                    //    foreach (Component.row r in comp.Table)
                    //    {
                    //        Word o = myOracle.OutputTrace(null);
                    //        r.rowValues.Add(null);
                    //    }
                    //}
                    throw new NotImplementedException();
                case CounterexampleHandlingPolicy.oneLocally:
                    //* 18-Add v to V of Cu′ ∈ C
                    //Word V2 = null;
                    //foreach (Component comp in components)
                    //{
                    //    comp.suffixes.Add(V2);

                    //}
                    //break;
                    throw new NotImplementedException();
            }
        }
        #endregion


        /// <summary>
        /// based on P.20 of the thesis
        /// </summary>
        /// <returns>The learnt conjecture</returns>
        public MealyMachine Learn()
        {
            //LearningLog.InitLogger();

            //* 1-Create component Cε = ⟨Σ ∪ {ε}, ε, Σ, ∅⟩
            Component c_e = new Component();
            //c_e.Table.Add(new Component.row(new Word()));
            foreach (ISymbol s in myOracle.InputAlphabet.AllSymbols())
            {
                c_e.suffixes.Add(new Word(s));
            }
            AddPrefixToComponent(c_e, new Word());

            //*  2-Init. components
            components = new List<Component>();
            components.Add(c_e);

            //* 3-Init. discrimination tree
            discrTree = new Tree<Word, ISymbol>(new Word());
            c_e.correspondingNode = discrTree.Root;

            while (true)
            {
                //* 5-Hypothesis construction
                MealyMachine conj = ClosePack();

                //* 6-Hypothesis verification
                Word counterexample = myOracle.EquivalenceQ(conj);
                //* 7-Counterexample?
                if (counterexample == null)
                {
                    //* 8-Then: done
                    return conj;
                }
                //* 11-Exploit counterexample ...
                HandleCounterexample(counterexample);
            }
        }
    }
}
